%!TEX root = paperEdit.tex
\section{Background}
\label{sec:background}

\vspace{-1ex}

%%% pkcs 11
\subsection{RSA PKCS\#11}

Security APIs implement access to sensitive
resources in a secure way. The design of such APIs is critical, as
they have to ensure the secure creation, deletion, importing and
exporting of a key from a device.  Also, they are responsible for
permitting the use of these keys for encryption, decryption, signing
and authentication so that even if a device is exposed to malicious
software the keys remain secure. The RSA PKCS\#$11$ standard specifies
an ANSI C API, called \textit{Cryptoki}, for hardware devices that can
perform cryptographic functions and store cryptographic-related and
encrypted data.  It aims to `sand-box' an application and isolate it
from the details of the underlying cryptographic device.

%\begin{table}
\begin{wraptable}[7]{r}{0.55\linewidth}
  \vspace{-5ex}
  \begin{scriptsize}
    \centering
  \begin{tabular}{l|l}
    \textbf{Function} & \textbf{Description} \\ \hline \hline
     \func{C\_logIn} & log a user to the token \\ \hline
	 \func{C\_GenerateKey} & generate a secret key \\ \hline
	 \func{C\_GenerateKeyPair} & generate a public/private key pair \\ \hline
	 \func{C\_WrapKey} & wrap (encrypt) a private key\\ \hline
	 \func{C\_UnwrapKey} & unwrap (decrypt) a private key\\ \hline	
  \end{tabular}
\end{scriptsize}
  \caption{RSA PKCS\#11 functions sample.}
  \label{pkcs:key-management}
%\end{table}
\end{wraptable}

When an application connects to a security token it
authenticates through a session. Sessions are uniquely identified
by a Cryptoki assigned value for a session handle to prevent a
`blind-repeat' of the same session: replaying the communication trace
of the session and replicating its functionality thereby bypassing all
the security mechanisms through repetition of the transmitted
information. The application can then access data in the token. RSA
PKCS\#11 provides a set of functions for \eg key, token, session and
object management, encryption, and decryption. Some example functions
are shown in Table~\ref{pkcs:key-management}.




%ieee

\begin{wraptable}[7]{r}{.55\linewidth}
  \vspace{-5ex}
  \centering
  \begin{scriptsize}
  \begin{tabular}{ l | l | l  }

\textbf{Session Type} &\textbf{ Required log-in} & \textbf{Operations} \\
\hline \hline 
Public &  no &Read Only\\ \hline
 Private & yes & Read Only \\ \hline
 Public  & no & Read-Write\\ \hline
 Private & yes & User Read-Write\\ \hline
 Private & yes & SO Read-Write \\ \hline

\end{tabular}
\end{scriptsize}
\vspace{-1ex}
   \caption{Cryptoki Session Types}
  \label{sessionTypes}
\end{wraptable}

Sessions are either public or private, defining the kind of objects
the application can access and the types of operations that it can
perform on them. The \func{C\_logIn} function is responsible for
allowing an application initiated either by a user, or a privileged
user termed a security officer (SO), to log into the token. An application
can start a private session only if the \func{C\_logIn} function is
called successfully. Sessions are also categorized as
\textit{read-only} or \textit{read-write} based on the operations the
application can perform. Public applications can only access
public data; private applications can access private and public data.
An application can change its session type, \eg from public to private
by logging in successfully; a private application can always revert to
a public session. Table~\ref{sessionTypes} presents the sessions and
transitions that RSA PKCS\#11 defines.

Authentication takes place only at the first
session and it is not required for the rest of the sessions. RSA
PKCS\#11 defines that all sessions that an application has with a
token must have the same state \ie when an application logs into a
token, then all application sessions with that token are logged in.
Logging in successfully to a token provides access to all
administrative, object management and cryptographic operations. If a
session deals with private keys, the corresponding operations can only
be executed if \func{C\_logIn} is called successfully. 
\eat{
A similar
approach is used for the flags\footnote{A boolean flag that is set to
  TRUE or FALSE. }, where the flag
$CKF\_Write\_Protected$\footnote{The token is \textit{write
    protected}: the application cannot create, modify, delete any
  object, token object or PIN within the token.} is true unless
\func{C\_logIn} is true.
}


    

%\begin{table}[h!]

%\end{table}





%%%12/11/2014

%% ISO/IEC 7816
\subsection{ISO/IEC 7816}

We focus on Part~4 of the ISO/IEC 7816
standard~\cite{7816-4}, which specifies the command-response pairs for
communication, the data and application structures in the card, means
for accessing and retrieving data, methods for secure messaging,
access rights to files and access methods to algorithms processed by
the card.
ISO 7816 supports: \begin{inparaenum}[(\itshape i\upshape)] 
\item Dedicated Files (DF) which host applications, group files
  and data objects. A DF may be the parent of other files
  (immediately under this DF).
\item Elementary Files (EF) which store data and cannot be parents of
  other files. An EF is either internal and stores data
  used by the card for management and control purposes; or working,
  and stores external data to be interpreted by the
  card.
\item Master File (MF), which is the DF at the root.
\end{inparaenum}
 
%\begin{table}[h!]
\begin{wraptable}[6]{r}{.45\linewidth}
  \vspace{-5ex}
  \centering 
  \begin{scriptsize}
  \begin{tabular}{  l | l   l  l  l  l  l  l }
  \textbf{Type} & \textbf{\texttt{Cla}}& \textbf{\texttt{Ins}} &
  \textbf{\texttt{P1}} & \textbf{\texttt{P2}} & \textbf{\texttt{Lc}} &
  \textbf{\texttt{Data}} & \textbf{\texttt{Le}} \\ \hline \hline
inter-industry & \val{00} & \val{84} & \val{00} & \val{00} & \val{00} & 
\val{00} & \val{08} \\
proprietary & \val{80} & \val{21} & \val{00} & \val{00} & \val{00} &
\val{00} & \val{08} 
\end{tabular}
\end{scriptsize}
  \caption{Implementations of the get$\_$challenge command.    }
  \label{ISO-getChallenge}
%\end{table}
\end{wraptable}
 
The communication unit consists of command-response pairs: a
\textit{command} is sent by the outside world to the card and a
\textit{response} is the card's reply. A command consists of a
compulsory 4-byte header, with the bytes named \texttt{Cla},
\texttt{Ins}, \texttt{P1} and \texttt{P2} and an optional body with
fields \texttt{Lc}, \texttt{Data} and \texttt{Le}. The \texttt{Cla}
field is the type of the command \ie inter-industry or proprietary.
The \texttt{Ins} field indicates the specific command, \eg the
\cmd{select\_file} command. Fields \texttt{P1} and \texttt{P2} are the
instruction parameters for the command, \eg the offset to write into
the selected file. The \texttt{Lc} is the number of bytes of the
\texttt{Data} field. The latter contains the data sent to the card.
Finally, \texttt{Le} is the number of the expected (if any) response
bytes. A response consists of an optional body, the response data, and
a compulsory 2-byte trailer of bytes \texttt{SW1} and \texttt{SW2}
encoding the expected status of the card after processing the
command). A command can
\begin{inparaenum}[(\itshape i\upshape)]
\item send data to the card; 
\item expect data from the card; 
\item both send and expect data; or
\item none of the above.
\end{inparaenum}
The length of the response depends on the sent command. The ISO 7816 standard
specifies the inter-industry command class for the \texttt{Cla} field, the
allowable values of the \texttt{Ins} field and the expected combinations of
values for the \texttt{P1}, \texttt{P2} and \texttt{SW1}, \texttt{SW2} fields
for all inter-industry commands/responses.



An APDU implementation is defined according to ISO 7816 and can either
be inter-industry, where the command codings are defined by the
standards; or proprietary, where the developers define their own
command codings. Table~\ref{ISO-getChallenge} presents an
inter-industry implementation of the get$\_$challenge command and a
possible proprietary one. Each byte of the inter-industry command can
be decoded, whereas the semantics of the proprietary command is
unknown. The inter-industry implementation has its \texttt{Cla} field
set to $00$ as ISO 7816 defines, so, the remaining fields can be
decoded. The proprietary one has an unknown
\texttt{Cla} code, so, it is not possible to determine the semantics
of the command using the ISO-based codings.
REPROVE aims to infer such unknown semantics.


\eat{
\begin{table}[h!]
  \centering 
  \begin{tabular}{  |l| l|  l|  l|  l|  l|  l| }
\hline
 \small CLA& \small INS& \small P1 & \small P2& \small Lc& \small Data Field& \small Le \\ 
\hline  \hline
\tiny 80 & \tiny 21& \tiny 00& \tiny 00 & \tiny 00&\tiny 00& \tiny 08 \\
 \hline
\end{tabular}
  \caption{Get-challenge command: proprietary implementation.}
  \label{proprietary-getChallenge}
\end{table}
}


 
\subsection{\func{C\_logIn} attacks}

A successful PIN verification authorizes access to private objects on
the token and to cryptographic functions. Once a user has been
authenticated she may perform any operation supported by the token
without restriction. So, compromising the \func{C\_logIn} function
allows to perform unauthorized operations over sensitive data. For
instance:
\begin{inparaenum}[(\itshape i\upshape)] 
\item misuse of session handles,  unencrypted
communication instead of encrypted or  performing a single authentication whereas a second one is required, 
may allow using old session handles for repeated access and blind
repeating a session;
\item the PIN being sent in plain text or revealed private data, allows sniffing the PIN, gaining unauthorized access to sensitive data and/or performing unauthorized 
operations on-card. 
\end{inparaenum}
Further attacks, which compromise a combination of the above  implementation issues, may lead to command injection, data injection, 
bypassing \func{C\_logIn} or  bypassing the communication mechanisms. 

\eat{\textit{etc.}.  \comment{Such insecure implementations allow
the following attacks:}{the above and the list below seem completely
disconnected. I suggest you spend time explaining them -- not everyone
reading this will have the background necessary to know what all these mean.}
\begin{inparaenum}[(\itshape i\upshape)]
\item use of old session handles for repeated access;
\item bypassing the \func{C\_logIn} command; 
\item sniffing for the PIN;
\item command and data injection;
\item repeating a session; and 
\item bypassing the communication mechanisms.
\end{inparaenum}}

 



\subsection{Reverse-engineering goals}

\eat{
From the APDU reverse-engineering we expect to infer how the low-level implementation
supports the high level abstractions. We must therefore answer the
following questions:
\begin{inparaenum}[(\itshape i\upshape)]
\item What is the semantics of the defined commands? For example,
  assume a proprietary command $c$. We want to define it in terms of
  the corresponding inter-industry command(s), decipher the meaning of
  $c$, \textit{etc}.
\item How is the protocol related to the RSA PKCS\#$11$ standard, \ie how
is a high-level command implemented by the low-level communication
mechanisms? 
%For example, when we send a \func{C\_logIn} command,
%what are the APDU commands and responses sent to/from the card?
\item Does the APDU allow the execution of commands that
RSA PKCS\#$11$ does not, \eg read sensitive keys?
\item Are key operations performed securely, \ie on-card?
\item Is sensitive data encrypted, \eg the token-library communication?
\item Is sensitive data exposed, \eg sensitive keys ?
\item Does all sensitive data have secure configurations? For example, can key
attributes be altered?
\end{inparaenum}
}


%\subsubsection{Inferred model}
\stitle{Inferred model}
REPROVE takes as input an APDU trace and produces a model
that describes the card's implementation of the communication
protocol. 
Reverse-engineering addresses three different abstractions of the protocol: the
exchanged commands, the executed on-card operations during the communication and the interconnection with specific RSA PKCS\#11
functions, with each addressing different types of attacks. 
For example:
\begin{compactitem}
\item Exchanged commands give insight into the semantics of the
  exchanged commands, may allow identifying parts of transmitted data
  of interest to the attacker, or gain knowledge of command semantics.
%of commands
%  that may lead to an attack and inject them, blind replay of sessions
%  as exchanged commands are known.
\item On-card operations %. As the on-card operations
  are mapped to a sequence of commands, so the attacker may have complete
  knowledge of the exact set of commands needed to execute
  unauthorized operations.
\item %Interconnection of the communication with PKCS\#11 functions.
  Since each of the PKCS\#11 function is recorded as sets of card
  operations, an attacker may be aware of which operations she needs
  to execute to perform already known PKCS\#11 attacks.
\end{compactitem} 

%\subsubsection{\func{C\_logIn} function} 
\stitle{\func{C\_logIn} function} 
The documentation of RSA
PKCS\#11 states that an application can access or perform any kind of
operation over sensitive data if and only if \func{C\_logIn} has been
called successfully.  Thus, we decided to present that function as a test case. 
% the initial evaluation
%of our proof-of-concept system 
 This gives insight on possible
vulnerabilities of a card, as security gaps in this function may allow
man-in-the-middle attacks. \eat{The outputs of REPROVE can be useful to
both the card suppliers and private users, in order to verify the
security of logging into a particular card. REPROVE aids in
understanding the security properties of the underlying
implementation.} Our technique is extensible and allows different
formal models to be plugged-in, depending on the security properties
needing to be checked.

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "paperEdit"
%%% End: 
